$\forall$$T$:Type, ${\it as}$,${\it bs}$,${\it cs}$,${\it ds}$:($T$ List).
\\[0ex](append(${\it as}$; ${\it cs}$) = append(${\it bs}$; ${\it ds}$) $\in$ ($T$ List))
\\[0ex]$\Rightarrow$ (($\parallel$${\it as}$$\parallel$ = $\parallel$${\it bs}$$\parallel$ $\in$ $\mathbb{Z}$) $\vee$ ($\parallel$${\it cs}$$\parallel$ = $\parallel$${\it ds}$$\parallel$ $\in$ $\mathbb{Z}$))
\\[0ex]$\Rightarrow$ guard(((${\it as}$ = ${\it bs}$) $\wedge$ (${\it cs}$ = ${\it ds}$)))